INDUCTION_tcom
12,41
postcript
pdf
Induction over naturals
=======================
Use nat_ind_a or comp_nat_ind_a normally.
Use tactics when require no wf subgoals
Us
involving goal being proved. (e.g. when proving
Us
wf lemmas).
origin
